\chapter{Choose your own problem: Antenna Placement}

\begin{quest}
	Inspired by: \url{http://www.lsi.upc.edu/~oliveras/TDV/practica-SMT.pdf}.
	
	On a long and thin island radio station antennae have to be placed. The island is divided into $R$ regions. Every region has to pay for the antennae installed inside of its boundaries, so the combined costs of the antennae must not be greater than this regions budget $B_r$. Furthermore every region also has demands regarding the combined popularity of the stations, $minScore_r$. The antennae, consequently, each have a price $P_a$ and a popularity score $S_a$. Furthermore it is the case that some pairs of antennae must not be placed closer than a specific minimum distance to each other. Finally, no antenna may be placed on the boundary between two regions.
	
	A specific instance of this problem is then:
	Given the boundaries, budget and minimum scores for every region, the cost and popularity score for every antenna and the specific minimum-distance requirements between pairs of antennae find a placement on the island that satisfies all of the above requirements.
\end{quest}


\section{General Introduction}
To the description above some things might be added for the sake of clarity. First, for all practical purposes the island is one-dimensional. This means that a region's boundaries simply are two numbers (the 'lower' kilometre and the 'higher' kilometre, where kilometre 0 means the starting point of the island). Following the text of the original exercise, a boundary is a shared point on the island. This means, if the first region is 30 kilometres long, it occupies kilometres 0 through 30. If this region is followed by another one which is 20 kilometres long this next one occupies kilometres 30 through 50 etc. An antenna is placed at kilometre $x$ of the island, which should lie inside of one of the region's boundaries. One cannot place more antennae than there are available (obviously) but one can place less (by assigning placements outside of the island's land mass). We shall first describe a general solution to these problems before presenting a special instance and its concrete solution (implemented and solved in through Yices).

\section{The Constraints}
We shall now distil and formalize the constraints indicated in the exposition. Contained here are only the purely formal constraints, not the actual Yices code implementing them. The reason for this is that due to some oddities in Yices' input language (or, of course, our insufficient mastery of its intricacies) one of these formal constraints typically corresponds to multiple functions occupying 30 or more lines of code.
 
\subsection{Minimum Score}
Every region demands a certain minimum combined score $minScore_r$ from the station antennae placed within its boundaries. Let $S_a$ be the score of antenna $a$, $\mathcal{AIR}_r$ the set of antennae in region $r$ and $\mathcal{R}$ the set of all regions. Then:

\begin{equation}
	\label{eq:task3_budget}
	\forall{r \in \mathcal{R}:} \left( \: \sum_{a \in \mathcal{AIR}_r} S_a \right) \geq minScore_r
\end{equation}


\subsection{Budget}
Every region has a budget $B_r$ and the combined costs of the antennae in its territory must not exceed this limit. In addition to the definitions given above, let $P_a$ be the price of antenna $a$ and $B_r$ the budget for region $r$. Then\footnote{Note the similarity to Equation \ref{eq:task3_budget}. The according functions and parts in the Yices source code share this similarity.}:

\begin{equation}
	\forall{r \in \mathcal{R}:} \left( \: \sum_{a \in \mathcal{AIR}_r} P_a \right) \geq B_r
\end{equation}



\subsection{No Placement On Borders}
No antenna may be placed directly on a border (we chose to include '0' in this definition as it, technically, also is a border). Let $\mathcal{A}$ be the set of all antennae, $Pos_a$ the position of antenna $a$ and $LBo_r$ and $UBo_r$ be the lower and upper boundary of region $r$ respectively. Then:

\begin{equation}
	\forall{a \in \mathcal{A}:} \nexists {r \in \mathcal{R}:} Pos_a = LBo_r \vee Pos_a = UBo_r
\end{equation}


\subsection{Minimum Distance}
For some pairs of antennae a minimum distance may be specified. Let $minDist_{a1,a2}$ be the minimum distance specified between $a1$ and $a2$ or 1 if no such distance is given and $a1 \neq a2$ or 0 otherwise. Then:

\begin{equation}
	\forall{a1, a2 \in \mathcal{A}:} |Pos_a1 - Pos_a2| \geq minDist_{a1,a2}
\end{equation}

\section{A Specific Problem}
After the general solution presented in the first part of this chapter we shall now deal with a specific instance of this problem. See the following tables for the details regarding the regions and antennae:

\begin{table}[htc]
% \usepackage{array} is required
\subfloat[Region data]{
\begin{tabular}{>{\centering\arraybackslash}p{0.22\textwidth}
>{\centering\arraybackslash}p{0.22\textwidth}
>{\centering\arraybackslash}p{0.22\textwidth}
>{\centering\arraybackslash}p{0.22\textwidth}}

Number & Upper-/Lower Boundary & Budget & Minimum Score \\ 
\hline 
0 & 0,30 & 13954 & 11 \\ 
1 & 30,52 & 12689 & 9 \\ 
2 & 52,74  & 9865 & 8 \\ 
\end{tabular} 
}
\vspace{5mm}

\subfloat[Antenna data]{
\begin{tabular}{>{\centering\arraybackslash}p{0.25\textwidth}
>{\centering\arraybackslash}p{0.25\textwidth}>
{\centering\arraybackslash}p{0.25\textwidth}}

Number & Popularity & Cost \\ 
\hline 
0 & 10 & 10457  \\ 
1 & 6 & 3737  \\ 
2 & 2  & 1187  \\ 
3 & 2  & 247  \\ 
4 & 9  & 8463  \\ 
5 & 9  & 7652  \\ 
6 & 6  & 6507  \\ 
\end{tabular} 
}
\caption{Input data}
\end{table}

Additionally, there are the constraints that the minimal distance between antennae 1 and 2 is 40 and that between antennae 1 and 5 is 37.

\subsection{Solution}

As we are dealing with a 'regular' satisfiability problem, no special methods are necessary. We run Yices, which tells us that there is a satisfying assignment of positions to antennae
(Table \ref{tab:solution}). To add palpability a visualisation can be seen in Figure \ref{fig:ant}.

\begin{table}[htc]
% \usepackage{array} is required
\begin{tabular}{>{\centering\arraybackslash}p{0.33\textwidth}
>{\centering\arraybackslash}p{0.33\textwidth}}

Antenna Number & Placed At\\ 
\hline 
1 & 14   \\ 
3 & 73   \\
4 & 53  \\ 
5 & 51  \\ 
6 & 13   \\ 
\end{tabular} 
\caption{Solution, antennae not mentioned here are unused}
\label{tab:solution}
\end{table}



\begin{figure}[htc]
	\begin{center}
		\includegraphics[width=\textwidth]{task_II_3_solution}

	\end{center}
	\caption{A solution to the problem found by Yices. Red = region border.}
	\label{fig:ant}
\end{figure}






























































